\begin{tabbing}
bframe{-}p(${\it es}$; $i$; $k$; $L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ \=($\forall$$l$:IdLnk. \+
\\[0ex]($\neg$($l$ $\in$ $L$ $\in$ IdLnk)) $\Rightarrow$ (es{-}sends(${\it es}$; $l$; $e$) = [] $\in$ (es{-}Msg(${\it es}$) List)))))
\-\-
\end{tabbing}